T:Type, L, L1, L2:T List. interleaving(T;L1;L2;L)  interleaving(T;L2;L1;L) 

latex

Definitions	x:A. B(x), {i..j}, t  T, P  Q, False, A, ij, ||as||, AB, True, T, , Prop, l[i], S  T, S  T, increasing(f;k), P & Q, x:A. B(x), disjoint_sublists(T;L1;L2;L), P  Q, P  Q, interleaving(T;L1;L2;L)
Lemmas	nat wf, disjoint sublists wf, increasing wf, select wf, not wf, length wf1, non neg length, int seg wf